\documentclass[a4paper,10pt]{article}

\usepackage{amsfonts, amsmath, amsthm, amssymb}
\usepackage[english]{babel}
%\usepackage{bookman}
%\usepackage{pxfonts}

%\usepackage[T1]{fontenc}
\usepackage{subfig}
\usepackage{graphicx}
\usepackage{lmodern}
\usepackage[utf8]{inputenc}
\usepackage{a4wide}
\pagestyle{headings}
\pagestyle{plain}
\usepackage{hyperref}

\usepackage{moreverb}
\usepackage{microtype}



\newcommand{\true}{\mathsf{true}}
\newcommand{\false}{\mathsf{false}}

\newcommand{\mint}[1]{\;\mathrm{#1}}
\newcommand{\then}{\Rightarrow}

\newcommand{\w}{\mathbf{w}}
\renewcommand{\c}{\mathbf{c}}
\newcommand{\1}{\mathbf{1}}


%\frenchspacing

\title{Automatic reasoning}
\author{Niklas Weber \\ 0841420, \\ Matúš Tejiščák \\ 4176200}
\date{\today}

\begin{document}

\maketitle

\newpage
\part{Truck loading}
\section{Representation}

Having $G$ goods and $N$ trucks, we can represent any solution as an $N \times G$ matrix $L$,
symbolizing that the truck $n$ carries $L_{ng}$ pallets of the goods $g$.
\begin{equation}
	L = \left(
	\begin{matrix}
		L_{11} & L_{12} & L_{13} & \cdots & L_{1G} \\
		L_{21} & L_{22} & L_{23} & \cdots & L_{2G} \\
		L_{31} & L_{32} & L_{33} & \cdots & L_{3G} \\
		       & \vdots &        & \ddots & \vdots \\
		L_{N1} & L_{N2} & L_{N3} & \cdots & L_{NG}
	\end{matrix} \right)
\end{equation}

We represent the weight of each goods as a column vector $\w$ of type $G \times 1$ and
the required count of pallets for each goods as a vector $\c$, also of type $G \times 1$.
\begin{equation}
	\w = \left(
	\begin{matrix}
		w_1 \\ w_2 \\ w_3 \\ \vdots \\ w_G
	\end{matrix} \right); \quad
	\c = \left(
	\begin{matrix}
		c_1 \\ c_2 \\ c_3 \\ \vdots \\ c_G
	\end{matrix} \right)
\end{equation}

Let us also use the name $w_{\max}$ for the maximum load of each truck and $c_{\max}$
for the maximum count of pallets for each truck. Then we have the following constraints:
\begin{align}
	L_{ng} &\geq 0
		& \text{(consistency of load)} \\
	L^T \cdot [1]_{N \times 1} &= \c
		& \text{(required count of pallets per each goods)} \\
	L \cdot [1]_{G \times 1} &\leq [c_{\max}]_{N \times 1}
		& \text{(space constraints for each truck)} \\
	L \cdot \w &\leq [w_{\max}]_{N \times 1}
		& \text{(weight constraints for each truck)}
\end{align}

This is all it takes to encode this problem. The length of the encoding is obviously
$O(NG)$, since we have three vector (in)equations, each dealing with a single matrix-time-vector
expression that is compared to another vector (the first inequality is obviously $O(NG)$).

\section{Implementation}

We solved this task using \textsf{Yices}, encoding the problem in a \textsf{Haskell} EDSL
designed for this purpose. In the \textsf{Haskell} program\footnote{
\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/Task1.hs}
}, we defined functions with rather
intuitive names instead of using direct matrix operations (although the functions essentially
don't encode anything more than matrix operations).

The \textsf{Haskell} EDSL gives us the convenience of expressing the formulas in a compact way
(using recursion, quantifiers, abstraction etc.), while it automatically expands the formulas
into first-order terms behind the scenes.

We also used a custom data type for the goods. Thus, we do not represent the goods using numbers
but using a specialized data type for readability.

Finding the maximum count of beer pallets was done by varying the beer-related component
of the vector $\c$ and seeing whether the resulting formula is still satisfiable.

\section{Solution}

We discovered that the maximum number of beer pallets that can be loaded is 19. A possible
load distribution in that case is given in Table \ref{tab:trucks} on page \pageref{tab:trucks}.

\begin{table}[htp]
	\centering{
	\begin{tabular}{cccccc}
		truck & cheese & beer & wine & drinks & chips \\
		1& 2&2&3&1&0 \\
		2& 1&6&0&0&0 \\
		3& 0&3&3&1&1 \\
		4& 0&1&1&4&2 \\
		5& 0&3&0&3&1 \\
		6& 1&4&1&1&1 \\
		\hline
		&4&19&8&10&5\\
	\end{tabular}
	}
	\caption{An optimal solution for the truck loading problem: we can load 19 pallets of beer.}
	\label{tab:trucks}
\end{table}

\newpage
\part{Solitaire}
\section{Representation of the game model}

\subsection{Variables}

We represent a single state of board of size $N \times N$ (and actions taken) by the following
collections of variables:
\begin{itemize}
	\item $S_{ij}$ is $\true$ iff there is a stone at the position $(i,j)$;
	\item $V = [v_i]$ represents the vertical coordinate of the \emph{selected stone}
		(ranging from $1$ to $N$);
	\item $H = [h_i]$ represents the horizontal coordinate of the \emph{selected stone}
		(ranging from $1$ to $N$);
	\item $d$ is the direction of skipping ($\true$ = horizontal, $\false$ = vertical);
	\item $s$ is the sign of skipping ($\true$ = towards higher coordinate values,
		$\false$ = towards lower coordinate values);
	\item $T = [t_i]$ is the number of steps taken from the beginning of the game.
\end{itemize}
The phrase \emph{selected stone} denotes (intuitively) the stone that will "skip" over its neighbor
to get from the current state to the next one (see Figure \ref{fig:selected}).

\begin{figure}[htp]
	\begin{center}
		\includegraphics[width=0.5\textwidth]{task2-selected}
	\end{center}
	\caption{Selected stone (red) "skipping" in different directions.}
	\label{fig:selected}
\end{figure}

Since we want to create a purely Boolean encoding of the problem, we will have to encode the integral
variables in binary. For this purpose, for each variable $X$, we introduce a sequence of
boolean variables $x_i$, along with the square-bracket notation:
\[ X = \sum_i 2^i x_i = [x_i] \mint{,} \]
where we implicitly identify $\true$ with $1$ and $\false$ with $0$. In practice, we limit the number
of the bits in question to $K = \lceil \log_2 (\mathsf{maxval}(X)+1) \rceil$.

In total, having a $N \times N$-sized board, we get
$N^2 + 3K + 2 = O(N^2)$ boolean variables.

The collection of  boolean variables $S_{ij}$ and $t_i$ describes the state of the playing board;
the variables
$V, H, d, s$ are nondeterministically chosen by the solver: they represent
the step taken by the player. Then $T'$ in the next step deterministically depends only on $T$
in the previous step; $S'_{ij}$ in the next step depends deterministically on
$S_{ij}, V, H, d$, and $s$ in the following way.

\subsection{Rules/clauses}

\subsubsection{Initial state}

The initial state is described by the following set of rules:
\begin{align}
	& [t_i] = 0
		& \text{(We start at the zero time.)} \\
	\bigwedge_{1 \leq i,j \leq N} & S_{ij} \Longleftrightarrow i \neq 3 \vee j \neq 3
		& \text{(Only the middle square is unoccupied.)}
\end{align}

\subsubsection{State transition}

First, let us list the short rules. 

\begin{align}
	\bigvee_{k=1}^{24-R} [t'_i] &= k-1 \wedge [t_i] = k
		& \text{(Time advances.)} \\
	\bigvee_{1 \leq i,j \leq N} [v_k] &= i \wedge [h_k] = j 
		& \text{($V$ and $H$ point into the board)} \\
	\bigwedge_{1 \leq i,j \leq N} [v_k] &= i \wedge [h_k] = j
		\; \Longrightarrow \; S_{ij} \wedge \neg S'_{ij} 
		& \text{(Stone removed from $(V,H)$.)} \\
\end{align}

The variables describing the new state always carry
a prime, that is, $S_{ij}$ belongs to the old state, $S'_{ij}$ belongs to the new state.
Let us continue with the jumping rule.

\begin{align}
	\bigvee &
	\left\lbrace \begin{array}{rl} 
		d \wedge      s \wedge
			& \displaystyle \bigvee_{\substack{1 \leq i \leq N \\ 1 \leq j \leq N-2}} 
			B(i,j,0,+1) \vspace{2mm} \\
		d \wedge \neg s \wedge
			& \displaystyle \bigvee_{\substack{1 \leq i \leq N \\ 3 \leq j \leq N}}
			B(i,j,0,-1) \vspace{2mm} \\
		\neg d \wedge      s \wedge
			& \displaystyle \bigvee_{\substack{1 \leq i \leq N-2 \\ 1 \leq j \leq N}}
			B(i,j,+1,0) \vspace{2mm} \\
		\neg d \wedge \neg s \wedge
			& \displaystyle \bigvee_{\substack{3 \leq i \leq N \\ 1 \leq j \leq N}}
			B(i,j,-1,0)
	\end{array} \right. & \text{(Four directions, four branches.)}
\end{align}

Here, for each direction (and each possible position) of we need to determine the next state of
the board. There are four directions the player could move in;
for every one of the four directions, there are $(N-2)^2$ stones that could be picked as
\emph{selected} (and we need to expand on that because we are working in a first-order theory).
\emph{At least} one of these possibilities must be true, hence the disjunctions. Also,
\emph{at most} one of these possibilities must be true but this is taken care of by the fact
that the possibilities themselves are mutually exclusive by their nature ($d$, $s$, $v_i$, $h_i$
are exactly determined in each).

Now we need to describe what rules must be observed in each of these four branches.
First, the selected stone must match. Then we describe how stones are affected by the skip.
Finally, we describe how the unaffected stones are carried to the new state unchanged.
\begin{align}
	B(i,j,p,q) &= [v_k] = i \wedge [h_k] = j \wedge A(i,j,p,q) \wedge U(i,j,p,q) \\
	A(i,j,p,q) &= S_{i+p,j+q} \wedge \neg S_{i+2p,j+2q}
		\wedge \neg S'_{i+p,j+q} \wedge S'_{i+2p,j+2q} \\
	U(i,j,p,q) &= \bigwedge_{1 \leq k,l \leq N}
		\underbrace{(k,l) \notin \{(i,j),(i+p,j+q),(i+2p,j+2q)\}}_{\text{unaffected}}
		\Longrightarrow
		S_{kl} \Leftrightarrow S'_{kl}
\end{align}

The nested quantifier used to describe the unaffected stones in $U(i,j,p,q)$ causes the
total number of clauses to blow up to $O(N^4)$.

\subsubsection{Final state}

If we denote the required number of stones to remain on the board $R$, then the final state
must satisfy this condition:
\begin{equation}
	[t_i] = 24 - R
\end{equation}
This exploits the fact that in each step we get exactly one stone off the board.

Furthermore, we must be unable to make another step. This is similar to the (reduced) transition
specification -- we must prove that none of the four possible movements from any selected square
is possible (this proposition is called \textsf{deadEnd} in the Haskell program).

\begin{align}
	\neg \bigvee &
	\left\lbrace \begin{array}{rl} 
			\displaystyle \bigvee_{\substack{1 \leq i \leq N \\ 1 \leq j \leq N-2}} 
			&P(i,j,0,+1) \vspace{2mm} \\
			\displaystyle \bigvee_{\substack{1 \leq i \leq N \\ 3 \leq j \leq N}}
			&P(i,j,0,-1) \vspace{2mm} \\
			\displaystyle \bigvee_{\substack{1 \leq i \leq N-2 \\ 1 \leq j \leq N}}
			&P(i,j,+1,0) \vspace{2mm} \\
			\displaystyle \bigvee_{\substack{3 \leq i \leq N \\ 1 \leq j \leq N}}
			&P(i,j,-1,0)
	\end{array} \right. \text{ \textbf{where} } \bigg [
	P(i,j,p,q) = S_{ij} \wedge S_{i+p,j+q} \wedge S_{i+2p,j+2q} \bigg ]
\end{align}

\subsection{Total number of clauses and variables}

\begin{itemize}
	\item $N^2 + 3K + 2 = O(N^2)$ Boolean variables
	\item $O(N^2) + O(N^4) + O(N^2) = O(N^4)$ clauses (initial state + transition + final state)
\end{itemize}
In total, we have $O(N^4)$ clauses and $O(N^2)$ Boolean variables.

\section{Implementation of the model}

\subsection{Binary encoding}

In our program, we only have binary encoding constraints of the shape
\begin{equation}
	[x_i] = X \mint{,}
\end{equation}
where $x_i$ is a collection of Boolean variables and $X$ is an integer. This can be
represented as
\begin{equation}
	\bigwedge_{0 \leq i \leq K-1} x_i \Longleftrightarrow \mathsf{bit}(X,i) = 1 \mint{.}
\end{equation}
Take, for example, $X = 11_{10} = 01011_{2}$. This translates to the following formula:
\begin{equation}
	\neg x_4 \wedge x_3 \wedge \neg x_2 \wedge x_1 \wedge x_0
\end{equation}
Furthermore, addition occurs in only one place in our program and even there it is the addition
of $1$. Instead of devising elaborate addition algorithms, we simply hardcode a table:
\begin{equation}
	\bigwedge_{1 \leq i \leq N^2} [t_i] = i-1 \Longrightarrow [t'_i] = i \mint{,}
\end{equation}
which translates to a collection of $N^2$ implications, exactly one applicable in each step.

\subsection{Variable ordering}

Since we use \textsf{bddsolve} for this problem, we also need to specify the order of variables.
We picked this order: $t_i$, $d$, $s$, $v_i$, $h_i$, $S_{ij}$, going from most the constrained
variables ($t_i$ is completely determined by a single meta-variable in the previous step),
through the variables that are valuated nondeterministically ($d$, $s$, $v_i$, and $h_i$) to
$S_{ij}$, that depends on the choice of all other variables.

\subsection{Implementation languages}

The bulk of the work was done in \textsf{Haskell}\footnote{
	\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/Task2-bdd.hs}
} using a specialized EDSL, which enabled us
to write the formulas in the same form as they appear in this paper. Expansion into first-order
formulas is done by the machinery underneath.

Since \textsf{bddsolve} uses a bit quirky way of naming variables (which is completely
understandable for small formulas but less suitable for larger developments), we also used
a small \textsf{Perl} program\footnote{
	\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/Task2-mogrify.pl}
} to change systematical variable names to their
\textsf{bddsolve}-compatible counterparts. This program also computes the ordering of variables
given to \textsf{bddsolve}.

\section{Solving the questions}

We used \textsf{bddsolve} along with the \textsc{Reach} logic to solve the formulas described
in this paper. \textsf{Bddsolve} proceeded safely over iterations and in a short time it
gave results.

\begin{description}
	\item[Is it possible to end with three stones?] ~ \\
		Yes, it is. See Figure \ref{fig:sample-game-3} on page \pageref{fig:sample-game-3}
		for one of the possible game paths. Ending with three separated stones in the bottom
		line, there is no way to continue from that position.
		
	\item[Is it possible to end with two stones?] ~ \\
		Yes, a two-stone ending is reachable as well, as shown in the Figure \ref{fig:sample-game-2}
		on page \pageref{fig:sample-game-2}.
	
	\item[Is it possible to end with only one stone?] ~ \\
		No. For one stone, \textsf{bddsolve} reports unsatisfiability of the problem, hence
		square peg solitaire with the usual rules (exactly one stone left) is unsolvable from our
		starting position. However,
		if we had started from a little different initial position (where the empty position would
		be off-center by one square, in one of the four directions), the game would	have been
		solvable.
\end{description}


\newpage
\subsection{Figures}
\begin{figure}[htp]
	\include{task2-appendix-3}
	\caption{An example game ending in three stones on the board.}
	\label{fig:sample-game-3}
\end{figure}

\begin{figure}[htp]
	\include{task2-appendix-2}
	\caption{An example game ending in two stones on the board.}
	\label{fig:sample-game-2}
\end{figure}
\newpage \part{Eleven Stones}
\section{The problem}
The question is: In how many ways can eleven stones be placed on a $11*11$ field, while being subject to certain constraints (see below)?

\section{Representation of the game model}
The question given suggests an implementation as a bddsolve problem. As such, we shall look for a model given only in first-order propositional (boolean) logic.

The board is represented by a $m*n$-matrix of boolean variables\footnote{Note, that this is a generalization of the original problem, which expressively states a $11*11$-matrix.}. $v\_a\_b$ means: there is a stone placed at point $(a,b)$\footnote{With $1 \leq a \leq m \text{ and } 1 \leq b \leq n$}.

We see, that there are three basic types of constraints.
\begin{enumerate}
\item Reserved positions: \\
$(2, y) \text{ for } y \leq 5$\\
$(x, 4) \text{ for } 4 \leq x \leq 8$\\
$(10, y) \text{ for } 4 \leq y \leq 11$\\
$(x, y) \text{ for } 2 \leq x \leq 8 \text{ and } 7 \leq y \leq 8$\\

\item Mutual exclusive positions:\\
Only one stone per row\\
Only one stone per column\\
Distance between each stone $> \sqrt{6}$

\item 11 stones are being placed
\end{enumerate}
Let us begin by inspecting the first type of constraint: reserved fields.\\
Let $R$ be the set of tuples $(a,b)$ for which holds: the position denoted by the tuple lies inside the field's boundaries and at least one of the 'reserved position' constraints is violated.
Then we can express the union of these constraints as:
\begin{align}
	\bigwedge_{(a,b) \in R} & \neg v\_a\_b
		& \text{(Reserved positions are unoccupied)}
\end{align}
Next we shall focus on the constraints of mutual exclusiveness. Effectively they can be translated as 'if there is a stone on $(a,b)$ then there must be no stone on $(a',b')$ because of the \{row/column/distance\} constraint'. If one has seen this, the three conditions can be encoded in a straightforward manner:
\begin{align}
	\bigwedge_{a,b}  &\left( v\_a\_b \Longrightarrow 
	\bigwedge_{a' \neq a} \neg v\_a'\_b \right)
		& \text{(No two stones in one column)} \\
	\bigwedge_{a,b}  &\left( v\_a\_b \Longrightarrow 
	\bigwedge_{b' \neq b} \neg v\_a\_b'\right)
		& \text{(No two stones in one row)} \\
	\bigwedge_{a,b}  &\left(v\_a\_b \Longrightarrow 
	% if distance^2 > 6, then "(a,b) =/= (a',b')" is superfluous
	\bigwedge_{(a-a')^2 + (b-b')^2 > 6} \neg v\_a\_b'\right)
		& \text{(Distance between each stone } > \sqrt{6} \text{)}
\end{align}
Of course these implications can be conflated into one by making a conjunction of all the consequents (i. e. illegal fields) belonging to one antecedent (i.e. field where the stone is placed).

A reduction in size can be achieved, if the reserved positions are left out. This is possible in two senses: First, should there be such a position in the antecedent all of the rules having this antecedent may be omitted (as then the antecedent is always false and the implication as a whole always true). Regarding the formalization above this would mean that, for example, a complete rule $(a,b) \Longrightarrow \neg (a',b') \wedge \neg (a'',b'') \wedge ...$ may be removed if $(a,b)$ is reserved.

Second, should there be such a position in the consequent this specific conjunct may be omitted (as then the consequent is always true, as is the implication as a whole). An example: if $(a,b) \Longrightarrow \neg (a',b') \wedge \neg (a'',b'') \wedge ...$ and we know that $(a',b')$ is reserved we can shorten the rule to $(a,b) \Longrightarrow \wedge \neg (a'',b'') \wedge ...$.\\
This also makes sense intuitively: rules of mutual exclusiveness add no information if at least one of the two positions involved is always empty.

The final formula, which is tested for satisfiability is formed by combining the formulae for reserved positions and mutual exclusiveness through conjunction.

The last constraint, that there are eleven stones to be placed, is rather unhandy when written out in a generalized way. The best we can concoct is to give a disjunction of every 11-tuple of (different) fields not containing reserved places. If, instead, we accept the premiss that we are, \textit{in concreto}, dealing with a $11*11$ field here and if we furthermore take the 1-per-column / 1-per-row constraints into account we can formulate a much simpler requirement:
\begin{align}
&\bigwedge_{1 \leq a \leq 11} \left( \bigvee_{1 \leq b \leq 11} v\_a\_b \right) & \text{(At least one stone is placed in every row)}
\end{align}
As now we have at least one stone per row and, by merit of the constraints, at most one stone per row we can be certain that the resulting valuation has exactly one stone for every row, which equals 11 stones.

This formalization forms the basis of our own implementation, as described below. 

\paragraph{Alternative formalization:} The crucial point is, that all of the constraints of mutual exclusiveness are symmetric. We can formalize this as:\\ $(a,b) \Rightarrow \neg (a',b') \Leftrightarrow (a',b') \Rightarrow \neg (a,b)$\\
Intuitively this makes sense, 'being in the same row as', 'being in the same column as' and 'having a distance $\leq \sqrt{6}$ to' are symmetric relations. This means, that we can construct a set of (unordered) pairs of positions. Every of these pairs describes two positions which may not be occupied simultaneously. Let $ME$ be this set. Then
\begin{align}
	\bigwedge_{((a,b), (a',b')) \in ME}  & \neg (v\_a\_b \wedge v\_a'\_b')  & 
			& \text{(No mutual exclusive pair)}
\end{align}
Again, pairs containing reserved positions can be filtered out (as then the negated conjunction would always be true).
We do think that this forms a minimal formalization. A second implementation based on this model has been developed, but time has been too limited to debug it properly.
\section{Implementation}
As indicated, this refers to the non-minimal model.
When looking at the formulae described above one may notice that non-standard expressions have only been used in the meta language used to describe big conjunctions. More precisely: they are only used for the ranges ($(a,b) \in R$ etc.). When one unfolds these expression the result is an ordinary first-order propositional logic formula.

This unfolding has been implemented by means of a Python script\footnote{\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/task3.py}}. We assume that a description of the Python code is outside of the focus of this document.
\section{Solution}
We have employed BDDSolve's \textsc{SAT} logic, applied to the formula generated by the Python script mentionend above. The variables are ordered lexicographically. This is a satisfying assignment found by BDDSolve:
\setcounter{MaxMatrixCols}{20}
\begin{figure}[htp]
	\begin{center}
	\include{task3-appendix-1}
	\end{center}
	
	\caption{A solution to the problem found by BDDSolve\\
	Legend: $\bullet$ = stone, $\cdot$ = not occupied, $-$ = reserved, ! = conflict (does not occur)}
	\label{fig:sol-1}
\end{figure}
\newpage \part{Filling the Grid}
\section{The problem}
In this task we look at a $18*12$ grid on which squares are being laid out. There always are one $7*7$, one $6*6$, two $5*5$ and three $4*4$ squares. The question is: How many $3*3$ squares can possibly fit in addition to the other parts?
\section{Representation of the model}
Intuitively, an upper boundary on this number can be established if the space could be used fully:
\[(18*12 - 7^2  - 6^2 - 2*5^2 - 3*4^2) / 3^2 \approx 3.67\]
Thus $3$ is the highest possible outcome, which supplies us with a first check of our implementation.
For the creation of a model we shall look at the generalized problem of a $m*n$ grid. Let furthermore $s = (s_1,s_2,s_3,...,s_n)$ be a vector, where $s_a$ is the size of a side of part $x$\footnote{N.B.: With 'parts' I mean the squares to be placed on the grid. As this is the nomenclature also used in the implementation it might be helpful to also use it in the model.}. This vector is known. As we shall later increase the number of parts in a stepwise manner to find the maximal satisfiable configuration it is a handy convention to say that the lower part numbers are reserved for the invariable parts. For our concrete instance of the problem this means: $s_1$ up to $s_7$ represent the given parts, everything above is one of the $3*3$ squares.

Let us now look at the variable part of this satisfiability question: the position of the parts. Let $p = (p_1,p_2,p_3,...,p_n)$ be a vector and $p_a$ be a tuple $(x_a,y_a)$, being the $x$ and $y$ coordinates for part $a$\footnote{Note the reverse order when compared to the $m*n$-notation used for matrices. It holds that $1 \leq x \leq n$ and $1 \leq y \leq m$}. The actual task now consists of two parts:
\begin{enumerate}
\item Pick a number $c$ of $3*3$ squares
\item Find out whether there are positions for the $7+c$ parts to be placed which abide by two constraints:
\begin{enumerate}
	\item Every part is placed inside of the boundaries of the grid
	\item No two parts overlap
\end{enumerate}
\end{enumerate}
The first part is what we shall do by hand (and, knowing that in this specific case there can be no solution greater than $c = 3$, this is quite feasible). The satisfiability of the constraints shall be checked automatically. Accordingly, we have to make them more precise. Let us thus now focus on their formalization.
\paragraph{Every part is placed inside of the boundaries of the grid:}
The right border of a part is given by starting position plus size of one side minus one\footnote{One might note that one unit of size is 'taken up' by filling the initial field. Furthermore it should be noticed that $(1,1)$ in our interpretation means the upper left field of the grid. To see an example for a possible grid see the solution further below.}. In terms of the original vectors:
\[a_{rBorder} = x_a + s_a - 1\]
The lower border is given likewise:
\[a_{lBorder} = y_a + s_a - 1\]
The constraint can now be expressed rather simply. Let $P$ be the set of parts. Then:
\begin{align*}
	\forall p \in P:&\\
	& x_p \geq 0~\wedge\\
	& y_p \geq 0 ~\wedge\\
	& x_p + s_p - 1\leq n ~\wedge\\
	& y_p + s_p - 1\leq m
\end{align*}

\paragraph{No two parts overlap:}
First, we make a simple observation: two parts do not overlap if a) one part is strictly higher than the other (meaning: its lower boundary is higher than the upper boundary of the second part) or b) one part is strictly more left than the other or c) both. We can express this as follows:\\
\begin{align*}
	\forall p_0, p_1 \in P: p_0 \neq p_1 \Rightarrow &\\
	& ((x_{p_0} < x_{p_1} \wedge x_{p_0} + s_{p_0} \leq x_{p_1}) ~\vee & \text{($p_0$ further left)}\\
	& (x_{p_1} < x_{p_0} \wedge x_{p_1} + s_{p_1} \leq x_{p_0})) & \text{($p_1$ further left)} \\
	& \vee\\
	& ((y_{p_0} < y_{p_1} \wedge y_{p_0} + s_{p_0} \leq y_{p_1}) ~\vee & \text{($p_0$ further down)}\\
	& (y_{p_1} < y_{p_0} \wedge y_{p_1} + s_{p_1} \leq y_{p_0})) & \text{($p_1$ further down)} 
\end{align*}
\section{Implementation}
We have implemented this problem as a Yices program, using its specification language\footnote{\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/task4.ys}}.
The number of $3*3$ parts can be freely chosen by changing one constant definition. To find our solution we start at 3 and lower this value until the either we have reached 0 or the formula becomes satisfiable.\\
The variable part of this problem (the positions of the individual parts) is implemented as an empty function:
\begin{verbatimtab}
(define part-position :: (-> nat pos))
\end{verbatimtab}
This can be read as: part-position is a function which, given a natural number, returns a position. The natural number in question is the index of part, ranging from 0 to 6 plus the number of $3*3$ squares. Please note that this diverges from the model given above, as now we start counting at 0. This also holds true for the position in the grid ($(0,0)$ being the upper left corner). The constraints now form constraints on the interpretation of this empty function.
The \textbf{first constraint} (positioned inside of the boundaries) is expressed as the following function:
\begin{verbatimtab}[4]
(define part-inside-boundaries :: (-> pos dim bool)
	(lambda (p::pos d::dim)
		(and  
			(<= (+ (select p x) (select d x)) 12)
			(<= (+ (select p y) (select d y)) 18) 
			(>= (select p x) 0) 
			(>= (select p y) 0) 
		)
	)
)
\end{verbatimtab}
This function is called for every part's position. Note here, that 11 and 17 are the original boundaries. 12 and 18 already include an added $+1$. This is an equivalent way of writing the original inequality from our model.

The \textbf{second constraint} (no overlap) has been implemented as follows:
\begin{verbatimtab}[4]
(define parts-do-not-overlap :: (-> pos dim pos dim bool)
	(lambda (p0::pos d0::dim p1::pos d1::dim)
		(or 
			(or 
				(and 
					(< (select p0 x) (select p1 x)) 
					(<= (+ (select p0 x) (select d0 x)) (select p1 x))
				) 
				(and 
					(< (select p1 x) (select p0 x)) 
					(<= (+ (select p1 x) (select d1 x)) (select p0 x))
				)
			)

			(or 
				(and 
					(< (select p0 y) (select p1 y))
					(<= (+ (select p0 y) (select d0 y)) (select p1 y))
				)
				(and 
					(< (select p1 y) (select p0 y)) 
					(<= (+ (select p1 y) (select d1 y)) (select p0 y))
				)
			)
		)
	)
)
\end{verbatimtab}
When comparing with the section above it can be seen that this is a direct translation of the original constraint. A minor modification: whether the two parts being tested for non-overlap are not identical is checked on a higher layer in the code. As this is trivial we shall omit it here.\\
The rest of the code is mainly bookkeeping, e. g. calling the no-overlap function for every pair of squares and setting up the logical context.
\section{Solution}
Using the method and implementation described above we have found the maximal number of $3*3$ squares for which the formula is satisfiable to be 2. A satisfying assignment is:
\begin{verbatim}
(= (part-position 0) (mk-record x::1 y::0))
(= (part-position 1) (mk-record x::6 y::12))
(= (part-position 2) (mk-record x::3 y::7))
(= (part-position 3) (mk-record x::1 y::13))
(= (part-position 4) (mk-record x::8 y::8))
(= (part-position 5) (mk-record x::8 y::4))
(= (part-position 6) (mk-record x::8 y::0))
(= (part-position 7) (mk-record x::0 y::10))
(= (part-position 8) (mk-record x::0 y::7))
\end{verbatim}
A visualization of this solution:
\begin{figure}[htp]
	\begin{center}
		\includegraphics[width=0.5\textwidth]{task3-viz1}
		%\includegraphics[width=0.5\textwidth]{task2-selected}
	\end{center}
	\caption{A solution to the problem found by Yices}
	\label{fig:sol-2}
\end{figure}


\end{document}
